\begin{tabbing}
w{-}discrete{-}constraint($w$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$i$, $x$:Id.\+
\\[0ex]($\uparrow$discrete($i$;$x$))
\\[0ex]$\Rightarrow$ \=(constant\_function(s($i$;0).$x$;$\mathbb{Q}$;$w$.T($i$,$x$))\+
\\[0ex]\& (\=$\forall$$k$:Knd, $v$:kindcase($k$; $a$.$w$.TA($i$,$a$); $l$,$t$.$w$.M($l$,$t$) ), $s$:EState($w$.T($i$)).\+
\\[0ex]constant\_function($s$($x$);$\mathbb{Q}$;$w$.T($i$,$x$))
\\[0ex]$\Rightarrow$ constant\_function(((w{-}machine($w$;$i$).2).1)($k$,$v$,$s$,$x$);$\mathbb{Q}$;$w$.T($i$,$x$))))
\-\-\-
\end{tabbing}